Make the repo's licensing single and consistent, matching the wokelangiser
reference policy and the merged iseriser pattern:

- Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README
  badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable
  governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX
  directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md).
- Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0,
  everything else -> MPL-2.0.
- READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in
  LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip.

Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the
"never use AGPL" estate policy, and the Contributor Covenant CoC.

Verified: standards/scripts/check-licence-consistency.sh passes; no residual
PMPL/Palimpsest self-claims remain.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

The src/interface/abi ABI was scaffolded from a template and never
compiler-checked. This makes all four modules typecheck cleanly under
Idris2 0.7.0 with zero errors and zero warnings, and adds real
machine-checked theorems.

Types.idr:
- thisPlatform: replaced unenabled %runElab with plain value (Linux).
- DecEq BQNPrimitive: replaced "No absurd" catch-all with explicit
  off-diagonal cases for every ordered distinct constructor pair;
  Arith/Compare diagonals decided via their Char field's decEq.
- DecEq Result: same explicit off-diagonal expansion.
- createHandle: solve the {auto So (ptr/=0)} obligation via Data.So.choose
  instead of leaving MkHandle's proof unsolved.
- rankNonNeg: prove r>=0 by casing on r (compare-based >= does not reduce
  symbolically).

Layout.idr:
- paddingFor: use Data.Nat.minus instead of Nat subtraction (no Neg).
- arraySizeMinHeader: discharge the ?hole with a genuine So proof via a
  geEight lemma over the reassociated header sum.
- Divides/decDivides: sound divisibility decision procedure.
- alignUpCorrect (unsound Refl) replaced by alignUpDivides via decDivides.
- StructLayout concrete value cbqnArrayDescLayout: supply erased proofs
  {sizeCorrect = Oh} and {aligned = DivideBy 2 Refl}.
- CABICompliant upgraded to carry a FieldsAligned witness; added
  decFieldsAligned and a sound checkCABI returning Either.
- offsetInBounds: honest Maybe (So ...) via choose instead of an unsound
  universally-quantified So.

Proofs.idr (new): export-level machine-checked theorems —
cbqnArrayDescCompliant (direct DivideBy witnesses), okIsZero,
nullPointerIsFour, numberTagIsZero, arrayTagIsSix, scalarSingleElement.

Build: added src/interface/abi/bqniser-abi.ipkg; moved flat modules into
src/interface/abi/Bqniser/ABI/ so paths match namespaces. .gitignore now
ignores **/build/, *.ttc, *.ttm.

No believe_me/assert_total/idris_crash/postulate/%hint/holes anywhere.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA